This invention relates to digital computing devices, and is more particularly directed to a non-von-Neumann type of computer, that is, one which does not employ a traditional means for executing a stored program. The invention is more specifically concerned with a lambda calculus computer which solves a problem stated as a linear representation of tree structures corresponding to expressions and computes a result based on the manipulation of the tree structure.
Conventional computers are uniformly of the von Neumann type, which rely on a program stored in memory which is executed under control of a program counter. According to the von Neumann principle, data and instructions are stored as bytes of binary data in identifiable memory cells in a random access memory. An arithmetic-logic unit performs logical operations (e.g., addition) on the data, based on the stored program instructions. These relate to fetching of the data between the respective memory cells to the arithmetic logic unit, and storing results in other memory cells in the memory.
Computer programming for von Neumann computers involves keeping track of a multitude of instructions and data and the memory locations in which they are stored, both before they are processed in the arithmetic-logic unit and thereafter. A minor error in the details of the program can lead to an inability to identify the specific locations in memory wherein large amounts of data and program instructions are stored. This problem can become quite manifest where there are complex branch programs, recursions, or the like. This inevitably requires extensive manual debugging of software.
In order to avoid the above problems with von Neumann type computers, it would be to advantage to start afresh and avoid the von Neumann stored program approach. In particular, it is to advantage to consider a lambda calculus approach to problem solving as a means to achieve speed and simplicity in the functioning of a computer.
Many abstract and theoretical calculating machines have been proposed to implement the lambda calculus as a machine language and to define its operational characteristics. None of these has been satisfactory, because the proposed system was incomplete, lacked certain necessary properties, such as reduction semantics, or led to implementations which were simply too inefficient to be a serious competitor to the von Neumann type computer. For instance, see D. A. Turner, "A New Implementation Technique for Applicative Languages", 9 Software Practice and Experience, 1979. Generally speaking, traditional user programs are difficult to translate into combinator expressions, and experience has shown that user programs transform into incomprehensible, more than linearly growing, very large combinator expressions, with the object code always being much larger than the source code.
Lambda Calculus was developed as a formal system of computation by Church. See A. Church, "The Calculi of Lambda Conversion," Annals of Mathematics Studies No. 6 Princeton University Press, 1941. An object of the present invention is to efficiently employ this formal system of computation as a machine code in a computer having a novel architecture for accommodating same. In this regard, systems have been proposed in L. Aiello and G. Prini, "An Efficient Interpreter for the Lambda Calculus", 23 Journal of Computer and System Sciences, 383-424, 1981.
An arbitrary Lambda Calculus expression may be represented in preorder as follows: ##EQU1## This expression is described in detail by H. P. Barendregt in his book entitled "The Lambda Calculus, its Syntax and Semantics," North-Holland Publishing Co., Amsterdam, Netherlands, 1981, 1984
The arbitrary Lambda Calculus expression contains a sequence of n bindings (i.e., .lambda.x.sub.i ; i is an integer, 0.ltoreq.i.ltoreq.n) followed by a sequence of m application nodes denoted by P, followed by what is referred to as the "head". The head can only be a variable or another Lambda expression. Following the head are m Lambda expressions of the same form just described.
The operational representation of Lambda expressions in a computer must be absolutely unique and safe; The possibility of confusion and collision of variable names cannot be tolerated. To avoid the possibility of confusion and collision, applicant employs a "binding indices" (also known as "De Bruijn indicies") method of representing the bound variables in the arbitrary expression. See N. G. De Bruijn, "Lambda-Calculus Notation With Nameless Dummies. A Tool For Automatic Formula Manipulation With Application to the Church-Rosser Theorem," Indag, Math., Vol. 34 1972.
The binding indices method is described as follows:
a bound variable x.sub.i is represented by the number of Lambda bindings (i.e., .lambda.x.sub.i) located between it and its binding occurrence (.lambda.x.sub.k). For example, the Lambda expression: EQU (.lambda.x.sub.1 .lambda.x.sub.2 .lambda.x.sub.3 .multidot.((x.sub.1 x.sub.2)x.sub.3)(.lambda.x.sub.4 .multidot.x.sub.4))
is written in its binding indice form as follows: EQU (.lambda..lambda..lambda..multidot.((21)0)(.lambda..multidot.0))
The binding indices depend only on the structure of the Lambda expression and are completely implementation independent. However, this method of expression lends itself to the inventive implementation technique to be described herein.
The operational representation of the Lambda expression using binding indices is: EQU H.fwdarw.{.lambda..sup.n P.sup.m HA.sup.m /#};n&gt;o,m.gtoreq.o EQU A.fwdarw.{.lambda..sup.n' P.sup.m' HA.sup.m' /#};n'.gtoreq.o,m'.gtoreq.o
where H is the head of the expression and the A's are the arguments.
All Lambda expressions of this representation may be expressed in the following form: EQU .lambda..sup.* P.sup.* .lambda..sup.* P.sup.* .lambda..sup.* P.sup.*. . . P.sup.* #args.sup.*
the symbol .lambda..sup.* represents a sequence of betas and the symbol P.sup.* represents a sequence of application nodes (aps), where (*) is an integer and may be equal to zero.
An arbitrary lambda expression may be represented in direct graph form. A sequence of bindings (.lambda.*) is represented by a 45 degree line from upper left to lower right, and a sequence of aps by a 45 degree line from upper right to lower left. Therefore, a terse representation of an arbitrary lambda expression is graphically represented as a zigzag line, as shown in FIG. 1. A zigzag line representation suppresses the details of the arguments (A's) associated with the Lambda expression.
The employment of Lambda expressions as a system of computation requires that complex Lambda expressions be reduced to simplified equivalent forms which are called normal forms. Two reduction rules have been developed for simplifying complex Lambda expressions, they are: EQU (Beta-Conversion rule) B:(.lambda.x.multidot.M)N; B reduces to [N/x]M
where [N/x]M means the consistent replacement of N for all occurrences of x in M. EQU (Eta-Conversion rule) .eta.: (.lambda.x.multidot.Mx);.eta. reduces to M (if there are no free occurrences of x in M).
A Lambda expression is called reducible if it contains at least one instance of either a Beta conversion rule or an Eta conversion rule, which is called a "redex". An expression containing no redexes is said to be in "Normal Form." An expression following the form of the Beta-Conversion rule is referred to as a "beta redex", and one following the form of the Eta-Conversion rule is referred to as an "eta-redex".
Returning to the graphical representation of an arbitrary Lambda expression in FIG. 1, it is observed that the zigzag line structurally has a plurality of folds associated with it. In FIG. 1, the folds projecting to the right are called betas-aps and those projecting to the left are called aps-betas. The structure of these folds are illustrated in FIG. 2. The corner of an aps-betas is a beta-redex. The corner of the aps-betas of FIG. 2 contains the beta-redex: EQU (.lambda.a.multidot.M)Aa,
where M may represent a Lambda expression.
A betas-aps fold does not contain a beta-redex, and therefore beta reduction cannot process this portion of the zigzag line. Thus, the zigzag line, or expression that it represents, will be smoothed out or transformed, into a single betas-aps graph, or equivalent expression by executing Beta-Conversions. A transformation technique that accomplishes this objective is referred to as "beta reduction-in-the-large".
Beta reduction-in-the-large can be described in terms of the graphical representation of an arbitrary Lambda expression. An aps-betas fold is cut from the zigzag line and moved down the zigzag. This graph manipulation does not change the meaning (i.e., an equivalence preserving transformation) of the zigzag as long as a copy of the cutout aps-betas fold is inserted, as a prefix, before all of the arguments pending from a sequence of aps located between the original and final positions of the cutout.
Beta reduction-in-the-large is illustrated in FIG. 3. The cut C--C in FIG. 3 is concerned with a maximum possible aps-betas groupings in the first occurring aps-betas fold of the zigzag line. The letters a through r denote generally arguments and variables ordinarily pending from an arbitrary Lambda expression graph.
The graph on the right in FIG. 3 illustrates that in the transformation, the cut C--C has been moved down the zigzag line to the farthest possible position, before the bindings q and r. In addition, the cut C--C has to be inserted before all depending arguments from k to p. This insertion is denoted by underlining in FIG. 3, except for argument m where the insert cut is explicitly shown as an example.
In the example of FIG. 3, the betas are exhausted before the aps. An example where the aps are exhausted before the betas is shown in FIG. 4. In this case, before a transformation is performed, an extension of cut C--C is made, as shown in FIG. 4 as cut D--D. This technique is called "eta extension in-the-large", and is graphically accomplished by inserting the new betas-aps j' k' k*j* in the zigzag line. Eta-extension is the application of the Eta-Conversion rule in reverse. Eta-extension in-the-large is a repeated application of the Eta-Conversion rule in reverse.
As can be seen from FIG. 3 and FIG. 4, the application of beta reduction in-the-large combined with eta-extension in-the-large, where appropriate, transforms an arbitrary zigzag line into a single betas-aps-betas-#-args graph.
The betas-# portion of the transformed expression operates as a selector function and is of the form: ##EQU2## The transformed expression therefore represents the application of the selector function to the arguments (args) of the transformed expression, yielding the selected mth argument: EQU (.lambda.x.sub.1 .lambda.x.sub.2. . . .lambda.x.sub.n .multidot.x.sub.m)a.sub.1 a.sub.2. . . a.sub.n .fwdarw.a.sub.m
This property of the transformed expression is conceptually equivalent to a look-up table in a data environment. The environment may be implemented as an array with index m accessing the appropriate location containing a pointer to the argument. The argument am may be a constant, variable, symbol or an expression. If it is an expression we obtain again, an arbitrary zigzag line and the procedure of applying beta reduction in-the-large and eta extension in-the-large is repeated for that new expression.
If the argument a is a variable, then the resulting transformed expression is a single betas-aps graph terminating in a variable. This resulting skeleton structure has the important property that it will not be altered by later transformation, no matter what reduction sequence takes place in the arguments pending to the right of the zigzag line (from the aps). Moreover, these arguments are independent from one another, i.e., no conversion rule will cause any two of these arguments to interact. Thus, this independence suggests an implementation whereby the order in which the argument is reduced does not affect the overall result; and the reduction of these arguments may be performed concurrently.
The reduction method herein described is termed "head order" reduction. It is closely related to the "head normal form" method as described in C. P., Wadsworth, Semantics and Pragmatics of the Lambda Calculus, Sept. 1971, PhD. Thesis, Univ. of Oxford, and the "Lazy Normal form" method as described by K. J. Greene, A Fully Lazy Higher Order Purely Functional Language with Reduction Semantics. CASE Center Technical Report No. 8503, Syracuse University.
A finished transformed expression, after selector operation (or lookup), is in the form of a betas-aps-index, i.e., a sequence of betas followed by a sequence of applications ending in a number that represents a bound variable. As indicated above, the arguments pending from this transformed expression are independent of one another and therefore can be reduced concurrently. This is possible if a copy of the appropriate environment is attached to each of the arguments. By virtue of the transformation technique, including beta reduction and eta reduction in-the-large, the appropriate environment is already attached to the arguments as prefixes.
The prefix portion of the augmented arguments can be conveniently represented as a pointer into one shared environment. An advantageous implementation performing the reductions on the arguments sequentially or concurrently would attempt to preserve this sharing property. Since environments expand and shrink, a naive sharing arrangement would lead to corruption if several arguments share a single environment. To solve this problem, an implementation approach must include proper control over the shrinking or cutting back of the environment.
A lambda calculus computer has been proposed previously by the same inventor in U.S. Pat. No. 3,646,523. That computer was intended for use with a new formal machine language based on the lambda calculus. In the computer, an input channel breaks up input data into character strings, a device assigns these strings into memory locations in a linear memory, and an associative memory, or "tablet" stores the character strings. The tablet assumes the program in the form of a tree, and accordingly includes an array of high-speed registers, with the nodes of the tree being given by some program corresponding to rows in the tablet and with the branches that extend from the nodes corresponding to tablet columns. The tablet addresses are accessed using associative techniques, and so the tablet is connected with input/output units and other devices to serve as a central communications device.
Another proposal is contained in this inventor's U.S. Pat. No. 4,075,689, which deals with a computer system adapted for reduction language, i.e., lambda calculus or combinators. That computer system employs stack registers to define sets of memory locations where expressions stored therein as strings can be shifted up or down. Access to a processor is provided to the memory cells at the top of the registers. The top cells of the registers are tested for instances of reduction rules, and reduction is carried out, if appropriate. The computing process takes place in such a manner that the reduction processor performs state transitions on the top cells of the registers, several times if necessary. This process is called string reduction. Because of its intrinsic structure, it is too inefficient for present day computing requirements.
It can be seen that neither of these schemes involves the use of a shared environment, and so there are no means provided to address an environment sequentially, or to monitor the free space available as the environment grows and shrinks.
General background on the logic and protocol of a lambda calculus reduction machine are contained in Ferdinand Hommes, "How to Use the Reduction Machine", Gesellshaft fr Mathematik und Datenverarbeitung MbH Bonn, Mar. 23, 1977.